ВЕРИФИКАЦИЯ ПРИЛОЖЕНИЙ IEC 61499 НА ОСНОВЕ МЕТОДА Model Checking 

Дубинин Виктор Николаевич, кандидат технических наук, доцент, кафедра вычислительной техники, Пензенский государственный университет, victor_n_dubinin@yahoo.com
Вяткин Валерий Владимирович, доктор технических наук, профессор, факультет электротехники и компьютерных наук, Оклендский университет (г. Окленд, Новая Зеландия), victor_n_dubinin@yahoo.com 

681.5 : 004.415.28 

Предлагается подход к верификации управляющих приложений международного стандарта IEC 61499 на основе метода Model Checking.
В рамках данного подхода предлагается формальная модель переходов состояний системы в виде правил изменения функций. Рассматривается демонстрационный пример. 

Ключевые слова

верификация, символьная модель, функциональный блок, стандарт IEC 61499

 Скачать статью в формате PDF

1. Кларк, Э. Верификация моделей программ: Model Checking / Э. Кларк, О. Грамберг, Д. Пелед. – М. : МЦНМО, 2002. – 416 с.
2. International Standard IEC 61499. Function blocks for industrial-process measurement and control systems. Part 1: Architecture // International Electrotechnical Commission. – Geneva, 2005. – 111 p.
3. Cadence SMV. – URL: http://www.kenmcmil.com/smv.html.
4. NuSMV – New Symbolic Model Checker. – URL: http://nusmv.irst.itc.it.
5. Yoo, J. A Verification Framework for FBD Based Software in Nuclear Power Plants / J. Yoo, S. Cha, E. Jee // 15th Asia-Pacific Software Engineering Conference (APSEC '08). – Beijing, 2008. – P. 385–392.
6. Vyatkin, V. A modelling approach for verification of IEC1499 function blocks using Net Condition/Event Systems / V. Vyatkin, H.-M. Hanisch // IEEE conference on Emerging Technologies in Factory Automation (ETFA'99). – Barcelona, Spain, 1999. – P. 261–270.
7. Дубинин, В. Н. Анализ расширенных NCES-сетей на основе метода Model
Checking / В. Н. Дубинин, Х.-М. Ханиш, В. В. Вяткин, С. К. Шестаков // Новые информационные технологии и системы : труды IX Международной научно-технической конференции (НИТиС’2010). – Пенза, 2010. – Ч. 2. – C. 20–48.
8. Dubinin, V. On Definition of a Formal Semantic Model for IEC 61499 Function Blocks / V. Dubinin, V. Vyatkin // EURASIP Journal on Embedded Systems. – 2008. – Vol. Article ID 426713. – P. 10.
9. Vyatkin, V. The IEC 61499 Standard and its Semantics / V. Vyatkin // IEEE Industrial Electronics Magazine. – 2009. – V. 3, Issue 4. – P. 40–48.
10. Gurevich, Y. Evolving Algebras 1993: Lipari Guide / Y. Gurevich // Specification and Validation Methods. – Oxford : Oxford University Press, 1995. – P. 9–36.
11. Dubinin, V. Using Prolog for Modelling And Verification of IEC 61499 Function Blocks and Applications / V. Dubinin, V. Vyatkin, H.-M. Hanisch // 11-th IEEE International Conference on Emerging Technologies and Factory Automation (ETFA 2006), Proceedings. – Prague, Czech Republic, 2006. – P. 774–781.